A:Type, op:(AAA), id:A, p, q:, E:({p..q}A). (op,id) p  i < q. E(i)  A 

latex

Up	groups 1
Definitions of Statement	(op,id) lb  i < ub. E(i)
Definitions	t  T, x:A. B(x), x. t(x), x(s), {i...}, True, T, ff, i  j < k, False, P  Q, P & Q, , P  Q, tt, P  Q, x f y, if b then t else f fi , Y, A  B, A, (op,id) lb  i < ub. E(i), {i..j}, P  Q, Dec(P), Unit, ,
Lemmas	int seg wf, decidable le, le wf, assert of le int, bnot of lt int, eqff to assert, bnot wf, le int wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, lt int wf